…ch the code (#144)

Three independent commits, each droppable on its own. Two fix gates that
could never fail; one fixes documentation that actively misdirects.

---

## 1. `docs:` — two files misstate the code they describe

### `PROOF-NEEDS.md`

Claimed *"1 `Admitted` in `proofs/coq/lambda/LambdaCNO.v` (y_not_cno)"*.
Measured against `absolute-zero 87902bb7`:

```
$ grep -rn "Admitted" absolute-zero --include=*.v | wc -l
0
$ grep -rn "^Axiom"  absolute-zero --include=*.v | wc -l
23
```

**Zero `Admitted`. Twenty-three `Axiom`s across 6 files.** The old
wording was wrong in *both* directions — it overstated the
incompleteness and understated the trusted base 23×.

> **Why this matters operationally:** an `Axiom` **passes** a "no
`sorry` / no `Admitted`" gate silently. Counting only `Admitted`
measures the wrong thing.

`y_not_cno` is a **KEPT AXIOM** with a written rationale
(`LambdaCNO.v:388-399`), not an unproven hole — and it is *not* the
"concrete, closable proof obligation" the old text claimed. The
in-source note explains it needs an invariant closed under the full
reduction congruence, or a coinductive/step-indexed argument.

The doc now defers to the **AXIOM AUDIT** already in
`physics/LandauerDerivation.v`, which is notably self-critical — it
records that `cno_zero_energy_dissipation_derived` is an axiom *despite
its `_derived` name*, and that the triage docs' "DISCHARGE" marks are
inaccurate.

**Promoted to the top of "What Needs Proving"** — the audit's own
SOUNDNESS WARNINGS: `prob_nonneg` and `prob_normalized` are false over
unconstrained function-type distributions, and
`shannon_entropy_maximum`'s inequality is **backwards** (asserts uniform
*minimises* entropy). All three are currently **unused** — cheap now,
expensive later.

### `aletheia/CLAUDE.md`

Said *"all core logic lives in `src/main.rs` (~950 lines)"* and *"don't
split into modules unless >1000 lines"*. It has been **5 modules / 995
lines** for a while, `main.rs` at 121. That instruction would tell the
next agent to **undo the existing structure**.

Also corrected: 23 workflows → 16; `flake.nix` listed but absent; 18
integration tests → 32. Added a prominent warning that those 16 nested
workflows have **never run** (root-only discovery) — the fault that let
this crate stay uncompilable for a month.

---

## 2. `fix(aletheia):` — the SHA-pinning check could never fail

```rust
if line.contains("@v") && !line.contains("@") {
```

`contains("@v")` **implies** `contains("@")`, so the second clause is
always false and `has_unpinned` could never be set. Proven before
changing anything:

```
uses: actions/checkout@v4    old_detects_unpinned=false
```

This is aletheia's Silver-level *"GitHub Actions SHA pinning"* check —
and pointedly, the exact check that would have caught
`SonarSource/sonarqube-scan-action@master`, the unpinned action that
broke this repo's Governance and CodeQL in #139.

Replaced with `uses_line_is_pinned`, requiring 40 hex chars after the
final `@`, which also:
- accepts the inline `- uses:` form (the estate's existing linter
anchors to line-start and misses it)
- ignores a trailing `# v7.0.1` provenance comment, so a correct pin
with a stale comment isn't a false positive
- exempts `./…` local actions/reusables and `docker://` refs

Also replaced `assert!(true)` in `test_file_exists` with a real
assertion, anchored on `env!("CARGO_MANIFEST_DIR")` so it is
deterministic regardless of CWD.

**Verified:** 29 unit tests (was 26) · `cargo fmt --check` clean ·
clippy 25 → 23. End-to-end `cargo run -- .` now reports `[FAIL] GitHub
Actions SHA pinning`, correctly finding the one genuinely unpinned
action — where before the fix it reported a pass.

Refs #125.

---

## 3. `fix(#99):` — root `Justfile` was a fake gate

```make
build:
    @echo "Build not configured yet"
```

`build`, `test`, `fmt`, `lint`, `clean` all printed a string and
**exited 0**. Wired to the same commands root `rust-ci.yml` runs, in the
same order, so `just check` means what CI means.

Two deliberate limits, documented **in the recipes** so nobody "fixes"
them:
- `test` is `--bins` only — the integration suite is a spec for a CLI
that doesn't exist; 27/29 fail by design (#124). Adding `--tests` would
make the bar green by breaking it.
- `lint` is not yet `-D warnings` (#125). When that closes it must be
added **here and to `rust-ci.yml` together**, so local and CI never
disagree.

**Verified by running them, not reading them:** `just deps-check` → `OK:
zero dependencies`; `just test` → 29 passed; `just check` → exit 0.

**And verified the gate can actually fail** — appending badly-formatted
Rust makes `just fmt` exit 1 while `just build` still exits 0; reverting
restores 0. A gate nobody has watched fail is not a gate.

Closes #99.

---

## Not in this PR

- **#124** — still blocked on the source-of-truth question for RSR
checks
- **`guix.scm`** identity/licence clobber — separate, more urgent: #143

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>